YES(O(1),O(n^2)) We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict Trs: { #equal(@x, @y) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , -(@x, @y) -> #sub(@x, @y) , div(@x, @y) -> #div(@x, @y) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' } Weak Trs: { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We add following dependency tuples: Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , eratos#1^#(nil()) -> c_7() , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , eratos#1^#(nil()) -> c_7() , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {1,2,3,4,7,10,12,13} by applications of Pre({1,2,3,4,7,10,12,13}) = {5,8,11,14}. Here rules are labeled as follows: DPs: { 1: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 2: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 3: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 4: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 5: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 6: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 7: eratos#1^#(nil()) -> c_7() , 8: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 9: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 10: filter#1^#(nil(), @p) -> c_10() , 11: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 12: filter#3^#(#false(), @x, @xs') -> c_13() , 13: filter#3^#(#true(), @x, @xs') -> c_14() , 14: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 15: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 16: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 17: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 18: #eq^#(nil(), nil()) -> c_18() , 19: #eq^#(#0(), #0()) -> c_19() , 20: #eq^#(#0(), #s(@y)) -> c_20() , 21: #eq^#(#0(), #neg(@y)) -> c_21() , 22: #eq^#(#0(), #pos(@y)) -> c_22() , 23: #eq^#(#s(@x), #0()) -> c_23() , 24: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 25: #eq^#(#neg(@x), #0()) -> c_25() , 26: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 27: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 28: #eq^#(#pos(@x), #0()) -> c_28() , 29: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 30: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 31: #mult^#(#0(), #0()) -> c_31() , 32: #mult^#(#0(), #neg(@y)) -> c_32() , 33: #mult^#(#0(), #pos(@y)) -> c_33() , 34: #mult^#(#neg(@x), #0()) -> c_34() , 35: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 36: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 37: #mult^#(#pos(@x), #0()) -> c_37() , 38: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 39: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 40: #sub^#(@x, #0()) -> c_40() , 41: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 42: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 43: #div^#(#0(), #0()) -> c_43() , 44: #div^#(#0(), #neg(@y)) -> c_44() , 45: #div^#(#0(), #pos(@y)) -> c_45() , 46: #div^#(#neg(@x), #0()) -> c_46() , 47: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 48: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 49: #div^#(#pos(@x), #0()) -> c_49() , 50: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 51: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {6} by applications of Pre({6}) = {5}. Here rules are labeled as follows: DPs: { 1: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 4: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 5: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 6: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 7: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 8: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 9: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 10: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 11: #eq^#(nil(), nil()) -> c_18() , 12: #eq^#(#0(), #0()) -> c_19() , 13: #eq^#(#0(), #s(@y)) -> c_20() , 14: #eq^#(#0(), #neg(@y)) -> c_21() , 15: #eq^#(#0(), #pos(@y)) -> c_22() , 16: #eq^#(#s(@x), #0()) -> c_23() , 17: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 18: #eq^#(#neg(@x), #0()) -> c_25() , 19: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 20: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 21: #eq^#(#pos(@x), #0()) -> c_28() , 22: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 23: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 24: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 25: #mult^#(#0(), #0()) -> c_31() , 26: #mult^#(#0(), #neg(@y)) -> c_32() , 27: #mult^#(#0(), #pos(@y)) -> c_33() , 28: #mult^#(#neg(@x), #0()) -> c_34() , 29: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 30: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 31: #mult^#(#pos(@x), #0()) -> c_37() , 32: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 33: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 34: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 35: #sub^#(@x, #0()) -> c_40() , 36: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 37: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 38: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 39: #div^#(#0(), #0()) -> c_43() , 40: #div^#(#0(), #neg(@y)) -> c_44() , 41: #div^#(#0(), #pos(@y)) -> c_45() , 42: #div^#(#neg(@x), #0()) -> c_46() , 43: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 44: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 45: #div^#(#pos(@x), #0()) -> c_49() , 46: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 47: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 48: eratos#1^#(nil()) -> c_7() , 49: filter#1^#(nil(), @p) -> c_10() , 50: filter#3^#(#false(), @x, @xs') -> c_13() , 51: filter#3^#(#true(), @x, @xs') -> c_14() , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We estimate the number of application of {5} by applications of Pre({5}) = {4}. Here rules are labeled as follows: DPs: { 1: eratos^#(@l) -> c_5(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 3: filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , 4: filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) , 5: filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , 6: #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , 7: #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , 8: #eq^#(::(@x_1, @x_2), nil()) -> c_16() , 9: #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , 10: #eq^#(nil(), nil()) -> c_18() , 11: #eq^#(#0(), #0()) -> c_19() , 12: #eq^#(#0(), #s(@y)) -> c_20() , 13: #eq^#(#0(), #neg(@y)) -> c_21() , 14: #eq^#(#0(), #pos(@y)) -> c_22() , 15: #eq^#(#s(@x), #0()) -> c_23() , 16: #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , 17: #eq^#(#neg(@x), #0()) -> c_25() , 18: #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , 19: #eq^#(#neg(@x), #pos(@y)) -> c_27() , 20: #eq^#(#pos(@x), #0()) -> c_28() , 21: #eq^#(#pos(@x), #neg(@y)) -> c_29() , 22: #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , 23: *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , 24: #mult^#(#0(), #0()) -> c_31() , 25: #mult^#(#0(), #neg(@y)) -> c_32() , 26: #mult^#(#0(), #pos(@y)) -> c_33() , 27: #mult^#(#neg(@x), #0()) -> c_34() , 28: #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , 29: #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , 30: #mult^#(#pos(@x), #0()) -> c_37() , 31: #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , 32: #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , 33: -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , 34: #sub^#(@x, #0()) -> c_40() , 35: #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , 36: #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , 37: div^#(@x, @y) -> c_4(#div^#(@x, @y)) , 38: #div^#(#0(), #0()) -> c_43() , 39: #div^#(#0(), #neg(@y)) -> c_44() , 40: #div^#(#0(), #pos(@y)) -> c_45() , 41: #div^#(#neg(@x), #0()) -> c_46() , 42: #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 43: #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 44: #div^#(#pos(@x), #0()) -> c_49() , 45: #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 46: #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , 47: eratos#1^#(nil()) -> c_7() , 48: filter#1^#(nil(), @p) -> c_10() , 49: filter#3^#(#false(), @x, @xs') -> c_13() , 50: filter#3^#(#true(), @x, @xs') -> c_14() , 51: mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , 52: #and^#(#false(), #false()) -> c_65() , 53: #and^#(#false(), #true()) -> c_66() , 54: #and^#(#true(), #false()) -> c_67() , 55: #and^#(#true(), #true()) -> c_68() , 56: #natmult^#(#0(), @y) -> c_85() , 57: #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , 58: #add^#(#0(), @y) -> c_52() , 59: #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , 60: #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 61: #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , 62: #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , 63: #positive^#(#0()) -> c_73() , 64: #positive^#(#s(@x)) -> c_74() , 65: #positive^#(#neg(@x)) -> c_75() , 66: #positive^#(#pos(@x)) -> c_76() , 67: #natdiv^#(#0(), #0()) -> c_69() , 68: #natdiv^#(#0(), #s(@y)) -> c_70() , 69: #natdiv^#(#s(@x), #0()) -> c_71() , 70: #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , 71: #negative^#(#0()) -> c_77() , 72: #negative^#(#s(@x)) -> c_78() , 73: #negative^#(#neg(@x)) -> c_79() , 74: #negative^#(#pos(@x)) -> c_80() , 75: #pred^#(#0()) -> c_57() , 76: #pred^#(#neg(#s(@x))) -> c_58() , 77: #pred^#(#pos(#s(#0()))) -> c_59() , 78: #pred^#(#pos(#s(#s(@x)))) -> c_60() , 79: #succ^#(#0()) -> c_61() , 80: #succ^#(#neg(#s(#0()))) -> c_62() , 81: #succ^#(#neg(#s(#s(@x)))) -> c_63() , 82: #succ^#(#pos(#s(@x))) -> c_64() , 83: #natdiv'^#(#0(), @y) -> c_89() , 84: #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , 85: #natdiv'^#(#underflow(), @y) -> c_91() , 86: #divsub^#(#0(), #0()) -> c_81() , 87: #divsub^#(#0(), #s(@y)) -> c_82() , 88: #divsub^#(#s(@x), #0()) -> c_83() , 89: #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , 90: #natadd^#(#0(), @y) -> c_87() , 91: #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , 92: #natsub^#(@x, #0()) -> c_92() , 93: #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } Weak DPs: { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { #equal^#(@x, @y) -> c_1(#eq^#(@x, @y)) , #eq^#(::(@x_1, @x_2), ::(@y_1, @y_2)) -> c_15(#and^#(#eq(@x_1, @y_1), #eq(@x_2, @y_2)), #eq^#(@x_1, @y_1), #eq^#(@x_2, @y_2)) , #eq^#(::(@x_1, @x_2), nil()) -> c_16() , #eq^#(nil(), ::(@y_1, @y_2)) -> c_17() , #eq^#(nil(), nil()) -> c_18() , #eq^#(#0(), #0()) -> c_19() , #eq^#(#0(), #s(@y)) -> c_20() , #eq^#(#0(), #neg(@y)) -> c_21() , #eq^#(#0(), #pos(@y)) -> c_22() , #eq^#(#s(@x), #0()) -> c_23() , #eq^#(#s(@x), #s(@y)) -> c_24(#eq^#(@x, @y)) , #eq^#(#neg(@x), #0()) -> c_25() , #eq^#(#neg(@x), #neg(@y)) -> c_26(#eq^#(@x, @y)) , #eq^#(#neg(@x), #pos(@y)) -> c_27() , #eq^#(#pos(@x), #0()) -> c_28() , #eq^#(#pos(@x), #neg(@y)) -> c_29() , #eq^#(#pos(@x), #pos(@y)) -> c_30(#eq^#(@x, @y)) , *^#(@x, @y) -> c_2(#mult^#(@x, @y)) , #mult^#(#0(), #0()) -> c_31() , #mult^#(#0(), #neg(@y)) -> c_32() , #mult^#(#0(), #pos(@y)) -> c_33() , #mult^#(#neg(@x), #0()) -> c_34() , #mult^#(#neg(@x), #neg(@y)) -> c_35(#natmult^#(@x, @y)) , #mult^#(#neg(@x), #pos(@y)) -> c_36(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #0()) -> c_37() , #mult^#(#pos(@x), #neg(@y)) -> c_38(#natmult^#(@x, @y)) , #mult^#(#pos(@x), #pos(@y)) -> c_39(#natmult^#(@x, @y)) , -^#(@x, @y) -> c_3(#sub^#(@x, @y)) , #sub^#(@x, #0()) -> c_40() , #sub^#(@x, #neg(@y)) -> c_41(#add^#(@x, #pos(@y))) , #sub^#(@x, #pos(@y)) -> c_42(#add^#(@x, #neg(@y))) , div^#(@x, @y) -> c_4(#div^#(@x, @y)) , #div^#(#0(), #0()) -> c_43() , #div^#(#0(), #neg(@y)) -> c_44() , #div^#(#0(), #pos(@y)) -> c_45() , #div^#(#neg(@x), #0()) -> c_46() , #div^#(#neg(@x), #neg(@y)) -> c_47(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#neg(@x), #pos(@y)) -> c_48(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #0()) -> c_49() , #div^#(#pos(@x), #neg(@y)) -> c_50(#negative^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , #div^#(#pos(@x), #pos(@y)) -> c_51(#positive^#(#natdiv(@x, @y)), #natdiv^#(@x, @y)) , eratos#1^#(nil()) -> c_7() , filter#1^#(nil(), @p) -> c_10() , filter#2^#(@xs', @p, @x) -> c_11(filter#3^#(#equal(mod(@x, @p), #0()), @x, @xs'), #equal^#(mod(@x, @p), #0()), mod^#(@x, @p)) , filter#3^#(#false(), @x, @xs') -> c_13() , filter#3^#(#true(), @x, @xs') -> c_14() , mod^#(@x, @y) -> c_12(-^#(@x, *(@y, div(@x, @y))), *^#(@y, div(@x, @y)), div^#(@x, @y)) , #and^#(#false(), #false()) -> c_65() , #and^#(#false(), #true()) -> c_66() , #and^#(#true(), #false()) -> c_67() , #and^#(#true(), #true()) -> c_68() , #natmult^#(#0(), @y) -> c_85() , #natmult^#(#s(@x), @y) -> c_86(#natadd^#(@y, #natmult(@x, @y)), #natmult^#(@x, @y)) , #add^#(#0(), @y) -> c_52() , #add^#(#neg(#s(#0())), @y) -> c_53(#pred^#(@y)) , #add^#(#neg(#s(#s(@x))), @y) -> c_54(#pred^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #add^#(#pos(#s(#0())), @y) -> c_55(#succ^#(@y)) , #add^#(#pos(#s(#s(@x))), @y) -> c_56(#succ^#(#add(#pos(#s(@x)), @y)), #add^#(#pos(#s(@x)), @y)) , #positive^#(#0()) -> c_73() , #positive^#(#s(@x)) -> c_74() , #positive^#(#neg(@x)) -> c_75() , #positive^#(#pos(@x)) -> c_76() , #natdiv^#(#0(), #0()) -> c_69() , #natdiv^#(#0(), #s(@y)) -> c_70() , #natdiv^#(#s(@x), #0()) -> c_71() , #natdiv^#(#s(@x), #s(@y)) -> c_72(#natdiv'^#(#divsub(@x, @y), #s(@y)), #divsub^#(@x, @y)) , #negative^#(#0()) -> c_77() , #negative^#(#s(@x)) -> c_78() , #negative^#(#neg(@x)) -> c_79() , #negative^#(#pos(@x)) -> c_80() , #pred^#(#0()) -> c_57() , #pred^#(#neg(#s(@x))) -> c_58() , #pred^#(#pos(#s(#0()))) -> c_59() , #pred^#(#pos(#s(#s(@x)))) -> c_60() , #succ^#(#0()) -> c_61() , #succ^#(#neg(#s(#0()))) -> c_62() , #succ^#(#neg(#s(#s(@x)))) -> c_63() , #succ^#(#pos(#s(@x))) -> c_64() , #natdiv'^#(#0(), @y) -> c_89() , #natdiv'^#(#s(@x), @y) -> c_90(#natdiv^#(#s(@x), @y)) , #natdiv'^#(#underflow(), @y) -> c_91() , #divsub^#(#0(), #0()) -> c_81() , #divsub^#(#0(), #s(@y)) -> c_82() , #divsub^#(#s(@x), #0()) -> c_83() , #divsub^#(#s(@x), #s(@y)) -> c_84(#divsub^#(@x, @y)) , #natadd^#(#0(), @y) -> c_87() , #natadd^#(#s(@x), @y) -> c_88(#natadd^#(@x, @y)) , #natsub^#(@x, #0()) -> c_92() , #natsub^#(#s(@x), #s(@y)) -> c_93(#natsub^#(@x, @y)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_5(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_6(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_8(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { filter#1^#(::(@x, @xs), @p) -> c_9(filter#2^#(filter(@p, @xs), @p, @x), filter^#(@p, @xs)) } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , eratos(@l) -> eratos#1(@l) , eratos#1(::(@x, @xs)) -> ::(@x, eratos(filter(@x, @xs))) , eratos#1(nil()) -> nil() , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() , #natsub(@x, #0()) -> @x , #natsub(#s(@x), #s(@y)) -> #natsub(@x, @y) } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We replace rewrite rules by usable rules: Weak Usable Rules: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Trs: { #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #sub(@x, #0()) -> @x , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , #add(#0(), @y) -> @y , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natdiv'(#0(), @y) -> #s(#0()) } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [0 0] x1 + [0 2] x2 + [1] [0 2] [0 0] [0] [#eq](x1, x2) = [1] [0] [*](x1, x2) = [2 0] x1 + [2 0] x2 + [0] [0 0] [2 0] [1] [#mult](x1, x2) = [1 0] x2 + [0] [0 0] [1] [-](x1, x2) = [1 0] x1 + [2] [2 1] [2] [#sub](x1, x2) = [1 0] x1 + [2] [2 1] [2] [div](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [2 2] [1 0] [0] [#div](x1, x2) = [2 0] x1 + [0] [2 2] [0] [eratos](x1) = [0] [0] [eratos#1](x1) = [0] [0] [::](x1, x2) = [1 0] x1 + [1 2] x2 + [0] [0 0] [0 1] [1] [filter](x1, x2) = [1 1] x2 + [0] [0 1] [0] [nil] = [0] [0] [filter#1](x1, x2) = [1 1] x1 + [0] [0 1] [0] [filter#2](x1, x2, x3) = [1 2] x1 + [1 0] x3 + [0] [0 1] [0 0] [1] [mod](x1, x2) = [1 0] x1 + [2] [2 1] [2] [#0] = [2] [0] [filter#3](x1, x2, x3) = [0 0] x1 + [1 0] x2 + [1 2] x3 + [0] [1 0] [0 0] [0 1] [0] [#false] = [1] [0] [#true] = [0] [0] [#add](x1, x2) = [1 0] x1 + [1 0] x2 + [1] [2 1] [2 1] [0] [#s](x1) = [1 0] x1 + [2] [0 0] [1] [#neg](x1) = [1] [0] [#pred](x1) = [2] [2] [#pos](x1) = [1] [0] [#succ](x1) = [0 0] x1 + [2] [1 0] [0] [#and](x1, x2) = [1] [0] [#divByZero] = [0] [0] [#natdiv](x1, x2) = [2 0] x1 + [0 0] x2 + [0] [0 0] [0 2] [2] [#positive](x1) = [2 0] x1 + [2] [0 0] [0] [#negative](x1) = [1] [0] [#divsub](x1, x2) = [1 0] x1 + [0 0] x2 + [1] [0 0] [1 0] [1] [#underflow] = [0] [0] [#natmult](x1, x2) = [2] [1] [#natadd](x1, x2) = [2 1] x1 + [2 1] x2 + [1] [0 0] [0 0] [1] [#natdiv'](x1, x2) = [2 0] x1 + [0 0] x2 + [2] [0 0] [0 2] [2] [#natsub](x1, x2) = [0] [0] [#equal^#](x1, x2) = [0] [0] [c_1](x1) = [0] [0] [#eq^#](x1, x2) = [0] [0] [*^#](x1, x2) = [0] [0] [c_2](x1) = [0] [0] [#mult^#](x1, x2) = [0] [0] [-^#](x1, x2) = [0] [0] [c_3](x1) = [0] [0] [#sub^#](x1, x2) = [0] [0] [div^#](x1, x2) = [0] [0] [c_4](x1) = [0] [0] [#div^#](x1, x2) = [0] [0] [eratos^#](x1) = [2 0] x1 + [1] [1 1] [0] [c_5](x1) = [0] [0] [eratos#1^#](x1) = [2 0] x1 + [1] [0 0] [0] [c_6](x1, x2) = [0] [0] [filter^#](x1, x2) = [0 2] x2 + [0] [1 0] [2] [c_7] = [0] [0] [c_8](x1) = [0] [0] [filter#1^#](x1, x2) = [0 2] x1 + [0] [0 0] [0] [c_9](x1, x2) = [0] [0] [filter#2^#](x1, x2, x3) = [0] [0] [c_10] = [0] [0] [c_11](x1, x2, x3) = [0] [0] [filter#3^#](x1, x2, x3) = [0] [0] [mod^#](x1, x2) = [0] [0] [c_12](x1, x2, x3) = [0] [0] [c_13] = [0] [0] [c_14] = [0] [0] [c_15](x1, x2, x3) = [0] [0] [#and^#](x1, x2) = [0] [0] [c_16] = [0] [0] [c_17] = [0] [0] [c_18] = [0] [0] [c_19] = [0] [0] [c_20] = [0] [0] [c_21] = [0] [0] [c_22] = [0] [0] [c_23] = [0] [0] [c_24](x1) = [0] [0] [c_25] = [0] [0] [c_26](x1) = [0] [0] [c_27] = [0] [0] [c_28] = [0] [0] [c_29] = [0] [0] [c_30](x1) = [0] [0] [c_31] = [0] [0] [c_32] = [0] [0] [c_33] = [0] [0] [c_34] = [0] [0] [c_35](x1) = [0] [0] [#natmult^#](x1, x2) = [0] [0] [c_36](x1) = [0] [0] [c_37] = [0] [0] [c_38](x1) = [0] [0] [c_39](x1) = [0] [0] [c_40] = [0] [0] [c_41](x1) = [0] [0] [#add^#](x1, x2) = [0] [0] [c_42](x1) = [0] [0] [c_43] = [0] [0] [c_44] = [0] [0] [c_45] = [0] [0] [c_46] = [0] [0] [c_47](x1, x2) = [0] [0] [#positive^#](x1) = [0] [0] [#natdiv^#](x1, x2) = [0] [0] [c_48](x1, x2) = [0] [0] [#negative^#](x1) = [0] [0] [c_49] = [0] [0] [c_50](x1, x2) = [0] [0] [c_51](x1, x2) = [0] [0] [c_52] = [0] [0] [c_53](x1) = [0] [0] [#pred^#](x1) = [0] [0] [c_54](x1, x2) = [0] [0] [c_55](x1) = [0] [0] [#succ^#](x1) = [0] [0] [c_56](x1, x2) = [0] [0] [c_57] = [0] [0] [c_58] = [0] [0] [c_59] = [0] [0] [c_60] = [0] [0] [c_61] = [0] [0] [c_62] = [0] [0] [c_63] = [0] [0] [c_64] = [0] [0] [c_65] = [0] [0] [c_66] = [0] [0] [c_67] = [0] [0] [c_68] = [0] [0] [c_69] = [0] [0] [c_70] = [0] [0] [c_71] = [0] [0] [c_72](x1, x2) = [0] [0] [#natdiv'^#](x1, x2) = [0] [0] [#divsub^#](x1, x2) = [0] [0] [c_73] = [0] [0] [c_74] = [0] [0] [c_75] = [0] [0] [c_76] = [0] [0] [c_77] = [0] [0] [c_78] = [0] [0] [c_79] = [0] [0] [c_80] = [0] [0] [c_81] = [0] [0] [c_82] = [0] [0] [c_83] = [0] [0] [c_84](x1) = [0] [0] [c_85] = [0] [0] [c_86](x1, x2) = [0] [0] [#natadd^#](x1, x2) = [0] [0] [c_87] = [0] [0] [c_88](x1) = [0] [0] [c_89] = [0] [0] [c_90](x1) = [0] [0] [c_91] = [0] [0] [#natsub^#](x1, x2) = [0] [0] [c_92] = [0] [0] [c_93](x1) = [0] [0] [c] = [0] [0] [c_1](x1) = [1 0] x1 + [0] [0 0] [0] [c_2](x1, x2) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_3](x1) = [1 0] x1 + [0] [0 0] [0] [c_4](x1) = [1 0] x1 + [0] [0 0] [0] This order satisfies following ordering constraints [#equal(@x, @y)] = [0 0] @x + [0 2] @y + [1] [0 2] [0 0] [0] >= [1] [0] = [#eq(@x, @y)] [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [1] [0] >= [1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(::(@x_1, @x_2), nil())] = [1] [0] >= [1] [0] = [#false()] [#eq(nil(), ::(@y_1, @y_2))] = [1] [0] >= [1] [0] = [#false()] [#eq(nil(), nil())] = [1] [0] > [0] [0] = [#true()] [#eq(#0(), #0())] = [1] [0] > [0] [0] = [#true()] [#eq(#0(), #s(@y))] = [1] [0] >= [1] [0] = [#false()] [#eq(#0(), #neg(@y))] = [1] [0] >= [1] [0] = [#false()] [#eq(#0(), #pos(@y))] = [1] [0] >= [1] [0] = [#false()] [#eq(#s(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#s(@x), #s(@y))] = [1] [0] >= [1] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#neg(@x), #neg(@y))] = [1] [0] >= [1] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #pos(@y))] = [1] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #0())] = [1] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #neg(@y))] = [1] [0] >= [1] [0] = [#false()] [#eq(#pos(@x), #pos(@y))] = [1] [0] >= [1] [0] = [#eq(@x, @y)] [-(@x, @y)] = [1 0] @x + [2] [2 1] [2] >= [1 0] @x + [2] [2 1] [2] = [#sub(@x, @y)] [#sub(@x, #0())] = [1 0] @x + [2] [2 1] [2] > [1 0] @x + [0] [0 1] [0] = [@x] [#sub(@x, #neg(@y))] = [1 0] @x + [2] [2 1] [2] >= [1 0] @x + [2] [2 1] [2] = [#add(@x, #pos(@y))] [#sub(@x, #pos(@y))] = [1 0] @x + [2] [2 1] [2] >= [1 0] @x + [2] [2 1] [2] = [#add(@x, #neg(@y))] [filter(@p, @l)] = [1 1] @l + [0] [0 1] [0] >= [1 1] @l + [0] [0 1] [0] = [filter#1(@l, @p)] [filter#1(::(@x, @xs), @p)] = [1 0] @x + [1 3] @xs + [1] [0 0] [0 1] [1] > [1 0] @x + [1 3] @xs + [0] [0 0] [0 1] [1] = [filter#2(filter(@p, @xs), @p, @x)] [filter#1(nil(), @p)] = [0] [0] >= [0] [0] = [nil()] [filter#2(@xs', @p, @x)] = [1 0] @x + [1 2] @xs' + [0] [0 0] [0 1] [1] >= [1 0] @x + [1 2] @xs' + [0] [0 0] [0 1] [1] = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] [mod(@x, @y)] = [1 0] @x + [2] [2 1] [2] >= [1 0] @x + [2] [2 1] [2] = [-(@x, *(@y, div(@x, @y)))] [filter#3(#false(), @x, @xs')] = [1 0] @x + [1 2] @xs' + [0] [0 0] [0 1] [1] >= [1 0] @x + [1 2] @xs' + [0] [0 0] [0 1] [1] = [::(@x, @xs')] [filter#3(#true(), @x, @xs')] = [1 0] @x + [1 2] @xs' + [0] [0 0] [0 1] [0] >= [1 0] @xs' + [0] [0 1] [0] = [@xs'] [#add(#0(), @y)] = [1 0] @y + [3] [2 1] [4] > [1 0] @y + [0] [0 1] [0] = [@y] [#add(#neg(#s(#0())), @y)] = [1 0] @y + [2] [2 1] [2] >= [2] [2] = [#pred(@y)] [#add(#neg(#s(#s(@x))), @y)] = [1 0] @y + [2] [2 1] [2] >= [2] [2] = [#pred(#add(#pos(#s(@x)), @y))] [#add(#pos(#s(#0())), @y)] = [1 0] @y + [2] [2 1] [2] >= [0 0] @y + [2] [1 0] [0] = [#succ(@y)] [#add(#pos(#s(#s(@x))), @y)] = [1 0] @y + [2] [2 1] [2] >= [0 0] @y + [2] [1 0] [2] = [#succ(#add(#pos(#s(@x)), @y))] [#pred(#0())] = [2] [2] > [1] [0] = [#neg(#s(#0()))] [#pred(#neg(#s(@x)))] = [2] [2] > [1] [0] = [#neg(#s(#s(@x)))] [#pred(#pos(#s(#0())))] = [2] [2] >= [2] [0] = [#0()] [#pred(#pos(#s(#s(@x))))] = [2] [2] > [1] [0] = [#pos(#s(@x))] [#succ(#0())] = [2] [2] > [1] [0] = [#pos(#s(#0()))] [#succ(#neg(#s(#0())))] = [2] [1] >= [2] [0] = [#0()] [#succ(#neg(#s(#s(@x))))] = [2] [1] > [1] [0] = [#neg(#s(@x))] [#succ(#pos(#s(@x)))] = [2] [1] > [1] [0] = [#pos(#s(#s(@x)))] [#and(#false(), #false())] = [1] [0] >= [1] [0] = [#false()] [#and(#false(), #true())] = [1] [0] >= [1] [0] = [#false()] [#and(#true(), #false())] = [1] [0] >= [1] [0] = [#false()] [#and(#true(), #true())] = [1] [0] > [0] [0] = [#true()] [#natdiv(#0(), #0())] = [4] [2] > [0] [0] = [#divByZero()] [#natdiv(#0(), #s(@y))] = [4] [4] > [2] [0] = [#0()] [#natdiv(#s(@x), #0())] = [2 0] @x + [4] [0 0] [2] > [0] [0] = [#divByZero()] [#natdiv(#s(@x), #s(@y))] = [2 0] @x + [4] [0 0] [4] >= [2 0] @x + [4] [0 0] [4] = [#natdiv'(#divsub(@x, @y), #s(@y))] [#divsub(#0(), #0())] = [3] [3] > [2] [0] = [#0()] [#divsub(#0(), #s(@y))] = [0 0] @y + [3] [1 0] [3] > [0] [0] = [#underflow()] [#divsub(#s(@x), #0())] = [1 0] @x + [3] [0 0] [3] > [1 0] @x + [2] [0 0] [1] = [#s(@x)] [#divsub(#s(@x), #s(@y))] = [1 0] @x + [0 0] @y + [3] [0 0] [1 0] [3] > [1 0] @x + [0 0] @y + [1] [0 0] [1 0] [1] = [#divsub(@x, @y)] [#natdiv'(#0(), @y)] = [0 0] @y + [6] [0 2] [2] > [4] [1] = [#s(#0())] [#natdiv'(#s(@x), @y)] = [2 0] @x + [0 0] @y + [6] [0 0] [0 2] [2] >= [2 0] @x + [6] [0 0] [1] = [#s(#natdiv(#s(@x), @y))] [#natdiv'(#underflow(), @y)] = [0 0] @y + [2] [0 2] [2] >= [2] [0] = [#0()] [eratos^#(@l)] = [2 0] @l + [1] [1 1] [0] >= [2 0] @l + [1] [0 0] [0] = [c_1(eratos#1^#(@l))] [eratos#1^#(::(@x, @xs))] = [2 0] @x + [2 4] @xs + [1] [0 0] [0 0] [0] >= [2 4] @xs + [1] [0 0] [0] = [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))] [filter^#(@p, @l)] = [0 2] @l + [0] [1 0] [2] >= [0 2] @l + [0] [0 0] [0] = [c_3(filter#1^#(@l, @p))] [filter#1^#(::(@x, @xs), @p)] = [0 2] @xs + [2] [0 0] [0] > [0 2] @xs + [0] [0 0] [0] = [c_4(filter^#(@p, @xs))] The strictly oriented rules are moved into the corresponding weak component(s). We are left with following problem, upon which TcT provides the certificate YES(O(1),O(n^2)). Strict DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) } Weak DPs: { filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } Obligation: innermost runtime complexity Answer: YES(O(1),O(n^2)) We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. DPs: { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) , 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Trs: { #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , #sub(@x, #0()) -> @x , #div(#0(), #0()) -> #divByZero() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , filter#3(#true(), @x, @xs') -> @xs' , #add(#neg(#s(#0())), @y) -> #pred(@y) , #pred(#pos(#s(#0()))) -> #0() , #and(#true(), #true()) -> #true() } Sub-proof: ---------- The following argument positions are usable: Uargs(c_1) = {1}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1}, Uargs(c_4) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA). [#equal](x1, x2) = [0 1] x2 + [0] [0 1] [0] [#eq](x1, x2) = [0 1] x2 + [0] [0 1] [0] [*](x1, x2) = [2 1] x2 + [0] [1 0] [0] [#mult](x1, x2) = [2] [0] [-](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [0 1] [1 0] [0] [#sub](x1, x2) = [2 0] x1 + [1 0] x2 + [0] [2 2] [0 2] [2] [div](x1, x2) = [0 1] x1 + [0] [0 1] [0] [#div](x1, x2) = [1] [0] [eratos](x1) = [0] [0] [eratos#1](x1) = [0] [0] [::](x1, x2) = [1 0] x2 + [2] [1 1] [2] [filter](x1, x2) = [1 0] x2 + [0] [0 1] [1] [nil] = [0] [1] [filter#1](x1, x2) = [1 0] x1 + [0] [0 1] [1] [filter#2](x1, x2, x3) = [1 0] x1 + [2] [1 1] [2] [mod](x1, x2) = [0 0] x1 + [0] [1 1] [0] [#0] = [2] [1] [filter#3](x1, x2, x3) = [1 1] x1 + [1 0] x3 + [0] [0 2] [1 1] [0] [#false] = [1] [1] [#true] = [0] [1] [#add](x1, x2) = [0 0] x1 + [1 0] x2 + [2] [1 0] [1 0] [0] [#s](x1) = [1 0] x1 + [1] [0 1] [1] [#neg](x1) = [0 0] x1 + [1] [0 1] [2] [#pred](x1) = [1 0] x1 + [0] [0 0] [1] [#pos](x1) = [1 0] x1 + [1] [0 1] [2] [#succ](x1) = [2] [2] [#and](x1, x2) = [0 0] x2 + [1] [0 1] [0] [#divByZero] = [0] [0] [#natdiv](x1, x2) = [0] [0] [#positive](x1) = [2 0] x1 + [1] [0 0] [0] [#negative](x1) = [2 0] x1 + [0] [0 0] [0] [#divsub](x1, x2) = [0] [0] [#underflow] = [0] [0] [#natmult](x1, x2) = [0 2] x2 + [0] [2 2] [0] [#natadd](x1, x2) = [1 1] x2 + [0] [2 1] [1] [#natdiv'](x1, x2) = [0] [0] [#natsub](x1, x2) = [0] [0] [#equal^#](x1, x2) = [0] [0] [c_1](x1) = [0] [0] [#eq^#](x1, x2) = [0] [0] [*^#](x1, x2) = [0] [0] [c_2](x1) = [0] [0] [#mult^#](x1, x2) = [0] [0] [-^#](x1, x2) = [0] [0] [c_3](x1) = [0] [0] [#sub^#](x1, x2) = [0] [0] [div^#](x1, x2) = [0] [0] [c_4](x1) = [0] [0] [#div^#](x1, x2) = [0] [0] [eratos^#](x1) = [1 1] x1 + [1] [0 0] [0] [c_5](x1) = [0] [0] [eratos#1^#](x1) = [1 1] x1 + [0] [0 0] [0] [c_6](x1, x2) = [0] [0] [filter^#](x1, x2) = [1 0] x2 + [2] [0 0] [0] [c_7] = [0] [0] [c_8](x1) = [0] [0] [filter#1^#](x1, x2) = [1 0] x1 + [1] [0 0] [0] [c_9](x1, x2) = [0] [0] [filter#2^#](x1, x2, x3) = [0] [0] [c_10] = [0] [0] [c_11](x1, x2, x3) = [0] [0] [filter#3^#](x1, x2, x3) = [0] [0] [mod^#](x1, x2) = [0] [0] [c_12](x1, x2, x3) = [0] [0] [c_13] = [0] [0] [c_14] = [0] [0] [c_15](x1, x2, x3) = [0] [0] [#and^#](x1, x2) = [0] [0] [c_16] = [0] [0] [c_17] = [0] [0] [c_18] = [0] [0] [c_19] = [0] [0] [c_20] = [0] [0] [c_21] = [0] [0] [c_22] = [0] [0] [c_23] = [0] [0] [c_24](x1) = [0] [0] [c_25] = [0] [0] [c_26](x1) = [0] [0] [c_27] = [0] [0] [c_28] = [0] [0] [c_29] = [0] [0] [c_30](x1) = [0] [0] [c_31] = [0] [0] [c_32] = [0] [0] [c_33] = [0] [0] [c_34] = [0] [0] [c_35](x1) = [0] [0] [#natmult^#](x1, x2) = [0] [0] [c_36](x1) = [0] [0] [c_37] = [0] [0] [c_38](x1) = [0] [0] [c_39](x1) = [0] [0] [c_40] = [0] [0] [c_41](x1) = [0] [0] [#add^#](x1, x2) = [0] [0] [c_42](x1) = [0] [0] [c_43] = [0] [0] [c_44] = [0] [0] [c_45] = [0] [0] [c_46] = [0] [0] [c_47](x1, x2) = [0] [0] [#positive^#](x1) = [0] [0] [#natdiv^#](x1, x2) = [0] [0] [c_48](x1, x2) = [0] [0] [#negative^#](x1) = [0] [0] [c_49] = [0] [0] [c_50](x1, x2) = [0] [0] [c_51](x1, x2) = [0] [0] [c_52] = [0] [0] [c_53](x1) = [0] [0] [#pred^#](x1) = [0] [0] [c_54](x1, x2) = [0] [0] [c_55](x1) = [0] [0] [#succ^#](x1) = [0] [0] [c_56](x1, x2) = [0] [0] [c_57] = [0] [0] [c_58] = [0] [0] [c_59] = [0] [0] [c_60] = [0] [0] [c_61] = [0] [0] [c_62] = [0] [0] [c_63] = [0] [0] [c_64] = [0] [0] [c_65] = [0] [0] [c_66] = [0] [0] [c_67] = [0] [0] [c_68] = [0] [0] [c_69] = [0] [0] [c_70] = [0] [0] [c_71] = [0] [0] [c_72](x1, x2) = [0] [0] [#natdiv'^#](x1, x2) = [0] [0] [#divsub^#](x1, x2) = [0] [0] [c_73] = [0] [0] [c_74] = [0] [0] [c_75] = [0] [0] [c_76] = [0] [0] [c_77] = [0] [0] [c_78] = [0] [0] [c_79] = [0] [0] [c_80] = [0] [0] [c_81] = [0] [0] [c_82] = [0] [0] [c_83] = [0] [0] [c_84](x1) = [0] [0] [c_85] = [0] [0] [c_86](x1, x2) = [0] [0] [#natadd^#](x1, x2) = [0] [0] [c_87] = [0] [0] [c_88](x1) = [0] [0] [c_89] = [0] [0] [c_90](x1) = [0] [0] [c_91] = [0] [0] [#natsub^#](x1, x2) = [0] [0] [c_92] = [0] [0] [c_93](x1) = [0] [0] [c] = [0] [0] [c_1](x1) = [1 1] x1 + [0] [0 0] [0] [c_2](x1, x2) = [1 1] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] [c_3](x1) = [1 1] x1 + [1] [0 0] [0] [c_4](x1) = [1 1] x1 + [0] [0 0] [0] This order satisfies following ordering constraints [#equal(@x, @y)] = [0 1] @y + [0] [0 1] [0] >= [0 1] @y + [0] [0 1] [0] = [#eq(@x, @y)] [#eq(::(@x_1, @x_2), ::(@y_1, @y_2))] = [1 1] @y_2 + [2] [1 1] [2] > [0 0] @y_2 + [1] [0 1] [0] = [#and(#eq(@x_1, @y_1), #eq(@x_2, @y_2))] [#eq(::(@x_1, @x_2), nil())] = [1] [1] >= [1] [1] = [#false()] [#eq(nil(), ::(@y_1, @y_2))] = [1 1] @y_2 + [2] [1 1] [2] > [1] [1] = [#false()] [#eq(nil(), nil())] = [1] [1] > [0] [1] = [#true()] [#eq(#0(), #0())] = [1] [1] > [0] [1] = [#true()] [#eq(#0(), #s(@y))] = [0 1] @y + [1] [0 1] [1] >= [1] [1] = [#false()] [#eq(#0(), #neg(@y))] = [0 1] @y + [2] [0 1] [2] > [1] [1] = [#false()] [#eq(#0(), #pos(@y))] = [0 1] @y + [2] [0 1] [2] > [1] [1] = [#false()] [#eq(#s(@x), #0())] = [1] [1] >= [1] [1] = [#false()] [#eq(#s(@x), #s(@y))] = [0 1] @y + [1] [0 1] [1] > [0 1] @y + [0] [0 1] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #0())] = [1] [1] >= [1] [1] = [#false()] [#eq(#neg(@x), #neg(@y))] = [0 1] @y + [2] [0 1] [2] > [0 1] @y + [0] [0 1] [0] = [#eq(@x, @y)] [#eq(#neg(@x), #pos(@y))] = [0 1] @y + [2] [0 1] [2] > [1] [1] = [#false()] [#eq(#pos(@x), #0())] = [1] [1] >= [1] [1] = [#false()] [#eq(#pos(@x), #neg(@y))] = [0 1] @y + [2] [0 1] [2] > [1] [1] = [#false()] [#eq(#pos(@x), #pos(@y))] = [0 1] @y + [2] [0 1] [2] > [0 1] @y + [0] [0 1] [0] = [#eq(@x, @y)] [filter(@p, @l)] = [1 0] @l + [0] [0 1] [1] >= [1 0] @l + [0] [0 1] [1] = [filter#1(@l, @p)] [filter#1(::(@x, @xs), @p)] = [1 0] @xs + [2] [1 1] [3] >= [1 0] @xs + [2] [1 1] [3] = [filter#2(filter(@p, @xs), @p, @x)] [filter#1(nil(), @p)] = [0] [2] >= [0] [1] = [nil()] [filter#2(@xs', @p, @x)] = [1 0] @xs' + [2] [1 1] [2] >= [1 0] @xs' + [2] [1 1] [2] = [filter#3(#equal(mod(@x, @p), #0()), @x, @xs')] [filter#3(#false(), @x, @xs')] = [1 0] @xs' + [2] [1 1] [2] >= [1 0] @xs' + [2] [1 1] [2] = [::(@x, @xs')] [filter#3(#true(), @x, @xs')] = [1 0] @xs' + [1] [1 1] [2] > [1 0] @xs' + [0] [0 1] [0] = [@xs'] [#and(#false(), #false())] = [1] [1] >= [1] [1] = [#false()] [#and(#false(), #true())] = [1] [1] >= [1] [1] = [#false()] [#and(#true(), #false())] = [1] [1] >= [1] [1] = [#false()] [#and(#true(), #true())] = [1] [1] > [0] [1] = [#true()] [eratos^#(@l)] = [1 1] @l + [1] [0 0] [0] > [1 1] @l + [0] [0 0] [0] = [c_1(eratos#1^#(@l))] [eratos#1^#(::(@x, @xs))] = [2 1] @xs + [4] [0 0] [0] >= [2 1] @xs + [4] [0 0] [0] = [c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs))] [filter^#(@p, @l)] = [1 0] @l + [2] [0 0] [0] >= [1 0] @l + [2] [0 0] [0] = [c_3(filter#1^#(@l, @p))] [filter#1^#(::(@x, @xs), @p)] = [1 0] @xs + [3] [0 0] [0] > [1 0] @xs + [2] [0 0] [0] = [c_4(filter^#(@p, @xs))] Consider the set of all dependency pairs DPs: { 1: eratos^#(@l) -> c_1(eratos#1^#(@l)) , 2: eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , 3: filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , 4: filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Processor 'matrix interpretation of dimension 2' induces the complexity certificate YES(?,O(n^2)) on application of dependency pairs {1,4}. These cover all (indirect) predecessors of dependency pairs {1,2,3,4}, their number of application is equally bounded. The dependency pairs are shifted into the corresponding weak component(s). We apply the transformation 'removetails' on the sub-problem: Weak DPs: { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { eratos^#(@l) -> c_1(eratos#1^#(@l)) , eratos#1^#(::(@x, @xs)) -> c_2(eratos^#(filter(@x, @xs)), filter^#(@x, @xs)) , filter^#(@p, @l) -> c_3(filter#1^#(@l, @p)) , filter#1^#(::(@x, @xs), @p) -> c_4(filter^#(@p, @xs)) } We apply the transformation 'usablerules' on the sub-problem: Weak Trs: { #equal(@x, @y) -> #eq(@x, @y) , #eq(::(@x_1, @x_2), ::(@y_1, @y_2)) -> #and(#eq(@x_1, @y_1), #eq(@x_2, @y_2)) , #eq(::(@x_1, @x_2), nil()) -> #false() , #eq(nil(), ::(@y_1, @y_2)) -> #false() , #eq(nil(), nil()) -> #true() , #eq(#0(), #0()) -> #true() , #eq(#0(), #s(@y)) -> #false() , #eq(#0(), #neg(@y)) -> #false() , #eq(#0(), #pos(@y)) -> #false() , #eq(#s(@x), #0()) -> #false() , #eq(#s(@x), #s(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #0()) -> #false() , #eq(#neg(@x), #neg(@y)) -> #eq(@x, @y) , #eq(#neg(@x), #pos(@y)) -> #false() , #eq(#pos(@x), #0()) -> #false() , #eq(#pos(@x), #neg(@y)) -> #false() , #eq(#pos(@x), #pos(@y)) -> #eq(@x, @y) , *(@x, @y) -> #mult(@x, @y) , #mult(#0(), #0()) -> #0() , #mult(#0(), #neg(@y)) -> #0() , #mult(#0(), #pos(@y)) -> #0() , #mult(#neg(@x), #0()) -> #0() , #mult(#neg(@x), #neg(@y)) -> #pos(#natmult(@x, @y)) , #mult(#neg(@x), #pos(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #0()) -> #0() , #mult(#pos(@x), #neg(@y)) -> #neg(#natmult(@x, @y)) , #mult(#pos(@x), #pos(@y)) -> #pos(#natmult(@x, @y)) , -(@x, @y) -> #sub(@x, @y) , #sub(@x, #0()) -> @x , #sub(@x, #neg(@y)) -> #add(@x, #pos(@y)) , #sub(@x, #pos(@y)) -> #add(@x, #neg(@y)) , div(@x, @y) -> #div(@x, @y) , #div(#0(), #0()) -> #divByZero() , #div(#0(), #neg(@y)) -> #0() , #div(#0(), #pos(@y)) -> #0() , #div(#neg(@x), #0()) -> #divByZero() , #div(#neg(@x), #neg(@y)) -> #positive(#natdiv(@x, @y)) , #div(#neg(@x), #pos(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #0()) -> #divByZero() , #div(#pos(@x), #neg(@y)) -> #negative(#natdiv(@x, @y)) , #div(#pos(@x), #pos(@y)) -> #positive(#natdiv(@x, @y)) , filter(@p, @l) -> filter#1(@l, @p) , filter#1(::(@x, @xs), @p) -> filter#2(filter(@p, @xs), @p, @x) , filter#1(nil(), @p) -> nil() , filter#2(@xs', @p, @x) -> filter#3(#equal(mod(@x, @p), #0()), @x, @xs') , mod(@x, @y) -> -(@x, *(@y, div(@x, @y))) , filter#3(#false(), @x, @xs') -> ::(@x, @xs') , filter#3(#true(), @x, @xs') -> @xs' , #add(#0(), @y) -> @y , #add(#neg(#s(#0())), @y) -> #pred(@y) , #add(#neg(#s(#s(@x))), @y) -> #pred(#add(#pos(#s(@x)), @y)) , #add(#pos(#s(#0())), @y) -> #succ(@y) , #add(#pos(#s(#s(@x))), @y) -> #succ(#add(#pos(#s(@x)), @y)) , #pred(#0()) -> #neg(#s(#0())) , #pred(#neg(#s(@x))) -> #neg(#s(#s(@x))) , #pred(#pos(#s(#0()))) -> #0() , #pred(#pos(#s(#s(@x)))) -> #pos(#s(@x)) , #succ(#0()) -> #pos(#s(#0())) , #succ(#neg(#s(#0()))) -> #0() , #succ(#neg(#s(#s(@x)))) -> #neg(#s(@x)) , #succ(#pos(#s(@x))) -> #pos(#s(#s(@x))) , #and(#false(), #false()) -> #false() , #and(#false(), #true()) -> #false() , #and(#true(), #false()) -> #false() , #and(#true(), #true()) -> #true() , #natdiv(#0(), #0()) -> #divByZero() , #natdiv(#0(), #s(@y)) -> #0() , #natdiv(#s(@x), #0()) -> #divByZero() , #natdiv(#s(@x), #s(@y)) -> #natdiv'(#divsub(@x, @y), #s(@y)) , #positive(#0()) -> #0() , #positive(#s(@x)) -> #pos(#s(@x)) , #positive(#neg(@x)) -> #neg(@x) , #positive(#pos(@x)) -> #pos(@x) , #negative(#0()) -> #0() , #negative(#s(@x)) -> #neg(#s(@x)) , #negative(#neg(@x)) -> #pos(@x) , #negative(#pos(@x)) -> #neg(@x) , #divsub(#0(), #0()) -> #0() , #divsub(#0(), #s(@y)) -> #underflow() , #divsub(#s(@x), #0()) -> #s(@x) , #divsub(#s(@x), #s(@y)) -> #divsub(@x, @y) , #natmult(#0(), @y) -> #0() , #natmult(#s(@x), @y) -> #natadd(@y, #natmult(@x, @y)) , #natadd(#0(), @y) -> @y , #natadd(#s(@x), @y) -> #s(#natadd(@x, @y)) , #natdiv'(#0(), @y) -> #s(#0()) , #natdiv'(#s(@x), @y) -> #s(#natdiv(#s(@x), @y)) , #natdiv'(#underflow(), @y) -> #0() } StartTerms: basic terms Strategy: innermost No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate YES(O(1),O(1)). Rules: Empty Obligation: innermost runtime complexity Answer: YES(O(1),O(1)) Empty rules are trivially bounded Hurray, we answered YES(O(1),O(n^2))